\begin{tabbing}
$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]retraction($T$;$f$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$. $R$($x$,$x$))
\\[0ex]$\Rightarrow$ \=($\forall$$x$, $y$, $z$:$T$.\+
\\[0ex]($x$ = $f$($y$))
\\[0ex]$\Rightarrow$ ($\neg$($x$ = $y$))
\\[0ex]$\Rightarrow$ $y$ is $f$$\ast$($z$)
\\[0ex]$\Rightarrow$ ($\forall$$u$:$T$. $y$ is $f$$\ast$($u$) $\Rightarrow$ $u$ is $f$$\ast$($z$) $\Rightarrow$ $R$($u$,$z$))
\\[0ex]$\Rightarrow$ $R$($x$,$z$))
\-\\[0ex]$\Rightarrow$ \{$\forall$$x$, $y$:$T$. $x$ is $f$$\ast$($y$) $\Rightarrow$ $R$($x$,$y$)\}
\end{tabbing}